// buffer_write_double(val)
// Writes a double to the buffer

buffer_write(buffer, buffer_f64, argument0)
